Here we prove that despite the previous undecidability result, 
\OG is decidable for $\evold{2}$ processes. 
That is,  
given 
a process $P$, a set of processes $M$, and 
a barb $\alpha$, 
there exists an algorithm to determine whether there exists a process $R \in \BC_P^M$ such that $R \barb{\alpha}^{k}$ holds.
The proof exploits appeals to the theory of well-structured transition systems (see Section \ref{s:wsts}).
We define  $\procleq$, an ordering on processes  which turns out to be 
a well-quasi-ordering and strongly compatible with respect to  $\pired$.
This will allow us to compute a finite basis for the set of
processes exhibiting   $\alpha$; such a set will 
turn out to be upward-closed with respect to  $\procleq$.

More precisely, the algorithm to determine if there exists $R \in \BC_P^M$ such that $R \barb{\alpha}^{k}$ consists of three steps:
\begin{enumerate}
\item We restrict the set of terms under consideration  to those reachable by any $R \in \BC_P^M$.  
We characterize this set by (a) considering the 
set of \emph{sequential subterms} in $\BC_P^M$, i.e., 
the subterms of $P$ and the processes in $M$ that do not have parallel composition or adaptable processes 
as their topmost operator (cf. Definition \ref{d:seqst})
and (b) 
%i.e., terms not having parallel or locations as their topmost operator, included in the term $P$ or in the terms in $M$ and (b) 
introducing the ordering $\procleq$ over 
a tree-like representation of the processes in such a set (cf. Definition \ref{d:order}).
%terms with the above properties.
\item  We then show that it is possible to compute the finite basis of the set of processes 
that expose $\alpha$ at least $k$ consecutive times (Lemma \ref{lem:decpred}).
\item  Finally, we show that it is possible to determine whether or not some process $R \in \BC_P^M$ is included in the set generated by the finite basis (Theorem \ref{th:badec}).
\end{enumerate}


The above strategy requires Kruskal's theorem (Theorem \ref{lem:kruskal}) on well-quasi-orde\-rings on trees.
Unlike other works exploiting the theory of well-structured transition systems for obtaining decidability results (e.g. \cite{Busi}),
in the case of $\evold{2}$ it  is not possible to find a bound on the ``depth'' of processes.   
As an example, consider the process 
$R = \component{a}{P} \parallel ! \update{a}{\component{a}{\component{a}{\bullet}}}.\nil $.
One possible evolution of $R$ is the following:
$$R \pired \component{a}{\component{a}{P}} \parallel ! \update{a}{\component{a}{\component{a}{\bullet}}}.\nil \pired \component{a}{\component{a}{\component{a}{P}}} \parallel ! \update{a}{\component{a}{\component{a}{\bullet}}}.\nil  \pired \ldots$$ 
and thus one obtains a process with an unbounded number of nested adaptable processes. %: $\component{a}{\component{a}{\dots a[P]}}$.
Nevertheless, not everything is lost and some regularity can be found also in our case. 
By mapping processes into particular forms of trees and then exploiting an ordering over those trees, 
it can be shown that this is indeed a well-quasi-ordering with strong compatibility, 
and that it has an effective pred-basis. This way, decidability of \OG  can be shown as sketched above.

We start by introducing some 
%terminology and 
auxiliary definitions. 


%\todo{perhaps move some of these definitions to the decidability section?}
%\begin{definition}[Normal Form/Parallel Processes]\label{d:nform}
%Let $P$ be an \evol{} process.
%We say that
% $P$ is in \emph{normal form} iff
%%$$P \equiv \prod_{i=1}^{l} P_i \parallel \prod_{j=1}^{m}\prod_{k=1}^{n_j} \component{a_j}{P'_{j,k}} $$
%$$P = \prod_{i=1}^{m} P_i \parallel \prod_{j=1}^{n} \component{a_j}{P'_{j}} $$
%  where, for $i \in \{1,\ldots,m\}$, $P_i$ is not in the form $Q \parallel Q'$ or $a[Q]$, 
%  and, for all $j \in \{1,\ldots,n\}$,  %${P'_{j,k}}$ 
%${P'_{j}}$ is in normal form.

\begin{definition}[Parallel Processes]\label{d:pps}
  Let $P = \prod_{i=1}^{m} P_i \parallel \prod_{j=1}^{n} \component{a_j}{P'_{j}}$ be an \evol{} process in normal form.
  The set of \emph{top-level, parallel processes} of $P$, is defined as 
%Given $P$ in normal form, we denote with $\Par(P)$ the  set 
$$\Par(P)= \{P_i \mid i \in [1..m] \} \cup \{ \component{a_j}{P'_{j}} \mid j\in [1..n]  \}$$ 
%of all processes in parallel at top level. 
This definition extends to sets of processes in normal form  in the expected way.
\end{definition}





%We begin with the definition of sequential subprocesses.
 \begin{definition}[Sequential Subprocesses]\label{d:seqst}
 Let $P$ be an \evold{2} process.
%Using $\mu$ to stand for an input or output prefix,  
The set of  sequential subprocesses of $P$, denoted 
 $\subp(P)$, is defined inductively as follows:
$$
 \begin{array}{ll}
 \subp(\pi.P) & =  \{\pi.P\}\cup \subp(P) ~~\text{if $\pi = a$ or $\pi = \outC{a}$}\\
 \subp(\update{a}{U}.Q) & =  \{ \update{a}{U}.Q \} \cup \subp(U) \cup \subp(Q)\\  
 \subp(\sum_{i \in I} \pi_i.P_i) & =  \big\{  \sum_{i \in I} \pi_i.P_i \big\} \cup \bigcup_{i \in I} \subp(\pi_{i}.P_i)\\
 \subp(!\pi.P)  & =   \{!\pi.P\} \cup \subp(P) \\
\subp(P \parallel Q) &  =  \subp(P)\cup\subp(Q)  \\
 \subp(\component{a}{P}) & =   \subp(P) \\
 \subp(\bullet) & =  \emptyset 
 \end{array}
$$
Observe that $\subp(\nil) = \subp(\sum_{i \in \emptyset} \pi_i.P_i)~=~\{ \nil \}$.
The definition extends to sets of processes as expected.
 \end{definition}
 
Notice that, since we are considering processes $P \in \evold{2}$ (which make use of update patterns that cannot include $\bullet$ in the scope of prefixes), $\subp(P)$ is a set of processes that are not update patterns, that is they cannot have free occurrences of $\bullet$.

\begin{definition}%\label{d:numap}
 Let $P$ be an \evold{2} process.
The set of  adaptable processes names occurring in $P$, denoted 
 $\cnames(P)$,  is inductively defined (by resorting, in general, to $\cnames(U)$ over \evold{2} update patterns $U$) as follows:
$$
 \begin{array}{ll}
\cnames(\component{a}{U}) &= \{a\}\cup \cnames(U) \\
 \cnames(\pi.P) & =  \cnames(P) ~~\text{if $\pi = a$ or $\pi = \outC{a}$}\\
 \cnames(\update{a}{U}.Q) & =  \cnames(U) \cup \cnames(Q)\\  
 \cnames(\sum_{i \in I}\pi_{i}.U_{i}) &= \bigcup_{i \in I}\cnames(\pi_{i}.U_{i}) \\  
  \cnames(! \pi.U) &= \cnames(\pi. U) \\
\cnames(U_{1} \parallel U_{2}) & =  \cnames(U_{1}) \cup \cnames(U_{2}) \\
\cnames(\bullet) & = \emptyset 
\end{array}
$$
 The definition extends to sets of processes as expected.
 \end{definition}

%%Furthermore, 
%The set $\cnames(P) = \{a[\ ] \mid \component{a}{Q} \text{ appears in } P\}$ 
%stands for the names of localities appearing in $P$.
%The definition of $\subp$ and $\cnames$ are extended
%to sets of processes
%in the expected way.
%Given a set of terms $M=\{T_1, \dots, T_n\}$,
%%process $P$,  
%we denote with $\nset{M}$ the set containing all the sequential subterms and the names of localities appearing in $M$:  $\nset{M} = \subp(M) \cup  \cnames(M)$. % \cup \{ t\} $. 

\begin{definition}
Given a set of \evold{2} processes $S$, %$M=\{T_1, \dots, T_n\}$, 
we define:
$$\nset{S} = \subp(S) \cup   \{a[\ ] \mid  a \in \cnames(S) \}$$
\end{definition}

We are now ready to define the tree denotation of a process.


% : intuitively the depth of a tree is given by the depth of the nesting of components. 
 %See Figure \ref{fig:proc2tree} for an example.

%\begin{figure}[t]
%\input{tree}
 %\caption{The tree denotation of the process $a.P \parallel \update{b}{Q} \parallel \component{b}{c.R \parallel \component{d}{e.S}}  \parallel \component{f}{g.T}$}\label{fig:proc2tree}
%\end{figure}

 \begin{definition}[Tree of a process]\label{def:tree}
  Let $P = \prod_{i=1}^{m} P_i \parallel \prod_{j=1}^{n} \component{a_j}{P'_{j}}$ be an \evold{2}  process in normal form.
%, i.e.  $$P = \prod_{i=1}^{m} P_i \parallel \prod_{j=1}^{n} \component{a_j}{P'_{j}}.$$ 
The tree denotation of $P$, denoted $\Tree(P)$, is a tree over $\nset{\{P\}} \cup \{\varepsilon\}$ and it
  is built as follows.
% \begin{enumerate}
  The root is labeled $\varepsilon$, and
  %\item The root 
  has $m+n$ children: the former $m$ are leaves labeled $P_1, \dots, P_m$, while the latter $n$ are subtrees recursively built from processes $P'_{1}, \dots, P'_{n}$, where the only difference is that their roots are labeled $a_1[\ ], \dots, a_n[\ ]$, respectively.
 %\end{enumerate}
 %Given a process $Q \in \evold{2}$ we denote with $\Tree(Q)$
%the set of the tree denotations of the normal forms of $Q$.

Given a set of \evold{2} processes $S$, ${\cal T}_{S}$ denotes the set of trees over $\nset{S} \cup \{\varepsilon\}$.

 \end{definition}

%Notice that if $P$ is a process in \evold{2} then $\Tree(P)$ is a tree over $\nset{P} \cup \{\epsilon\}$.
%
\begin{example}

Let $P$ be the process $a.P_{1} \parallel \update{b}{Q} \parallel \component{b}{c.R \parallel \component{d}{\ }}  \parallel \component{f}{g.T}$.
Given Definition \ref{def:tree}, $\Tree(P)$ is depicted in Figure \ref{fig:uno}.
\end{example}
\begin{figure}[t]
\centering
 \linefigure 

\subfigure[A tree denotation]{\label{fig:uno}\includegraphics[width=0.4\textwidth]{extree.pdf}} 
\quad
\subfigure[Tree embedding]{\label{fig:due}\includegraphics[width=0.4\textwidth]{trees.pdf}}

\caption{Tree denotations for \evold{2} processes.} %of the process $a.P \parallel \update{b}{Q} \parallel \component{b}{c.R \parallel \component{d}{\ }}  \parallel \component{f}{g.T}$}
\label{fig:proc2tree}
 \linefigure
\end{figure}
 



We now define the ordering $\preceq$ on processes. 
It corresponds to the extension of $=$, %, first to sequences of elements in $\nset{S}^*$ and then 
 as described in Definition \ref{def:prectr}, to trees.
 Notice that when $=$ is extended to trees it is no longer a symmetric relation.
More precisely: %,  given
 \begin{definition}[Ordering $\preceq$]\label{d:order}
 Let $P$ and  $Q$ be \evold{2} processes.
 Also, let $=^{\mathsf{tr}}$ stand for the extension of $=$ as in  Definition \ref{def:prectr}. 
 Then we decree:
$P \preceq Q$ iff %there exists  $T' \in \Tree(P)$ and $T'' \in \Tree(Q)$ such that $T' =^{\mathsf{tr}} T''$.
$\Tree(P) =^{\mathsf{tr}} \Tree(Q)$.
 \end{definition}

In other words, given two processes $P$ and $Q$ such that $\Tree(P) =^{\mathsf{tr}} \Tree(Q)$, one simply checks if all the labels of $\Tree(P)$ occur in $\Tree(Q)$ and respect the ancestor relation. 

\begin{example}
Let $S$ and $T$ be the processes defined as
\begin{align*}
 S & =  a.P \parallel \component{b}{c.Q}\\
 T & = a.P \parallel \component{d}{ \component{b}{\component{f}{e.R \parallel c.Q}}}
 \end{align*}
 Then we have $S \preceq T$; tree denotations for both processes (and the injection between them) are depicted in Figure \ref{fig:due}.


\end{example}

We write $P \pired \succeq Q$ if there is some $P'$ such that $P \pired P'$ and $P' \succeq Q$.
We now define the set of all derivatives of a given \evold{2} process and show that $\preceq$ is a wqo over it.

\begin{definition}
Given an \evold{2} process $P$, we define $\deriv{P} =\{Q \mid P \pired ^* Q \}$.
This definition is extended to sets of processes in the expected way.
\end{definition}


We start by showing that given a set of processes $S$, $=^{\mathsf{tr}}$ is  a wqo over ${\cal T}_{S}$.

%By Proposition \ref{prop:eqwqo} and by noticing that set $\nset{M}$ is finite we have  that  = is a wqo over $\nset{M} \cup \{\epsilon\}$.
% By Lemma \ref{lem:Higman}, and since $=$ is a wqo on $\nset{S}$,  $=^*$ is a wqo over $\nset{S}^*$.
% Moreover, by Lemma \ref{lem:kruskal}, $=^{\mathsf{tr}}$ is a wqo over ${\cal T}_M$. 

 \begin{theorem} \label{th:wqoccs}
  Let $S$ be a set of $\evold{2}$ processes. Then, relation $=^{\mathsf{tr}}$ is a wqo over ${\cal T}_{S}$.
 \end{theorem}
\begin{proof}
The set $\nset{S}$ is finite by construction. 
Hence, by Proposition \ref{prop:eqwqo}, equality is a wqo over $\nset{S} \cup \{\varepsilon\}$.
Finally, since $=$ is a wqo, 
using Kruskal's Theorem (Theorem \ref{lem:kruskal}) we infer that 
$=^{\mathsf{tr}}$ is a wqo over ${\cal T}_{S}$. 
%\qed
\end{proof}


We now prove that the trees constructed from processes contained in the set of all derivatives form a subset of ${\cal T}_{S}$.
%We need an auxiliary definition.
\input{app-auxdef}

\begin{lemma} \label{lem:deriv}
 Let $P$ be an \evold{2} process. If  $P \pired Q$ then $\Tree(Q) \in {\cal T}_{\{P\}}$.
\end{lemma}
\begin{proof}
By induction on %the rule used to infer $\pired$.
the height of the derivation tree for $P \pired Q$, with a case analysis in the last rule used.
There are seven cases to check. 
%Let $Q$ be a process such that  $P \pired Q$. 
We recall that $\Tree(Q) \in {\cal T}_{\{P\}}$ iff $\Tree(Q)$ is over $\nset{P} \cup \{\varepsilon\}$.
\begin{description}
\item[Case \rulename{Act1}]
Then $P = P_{1} \parallel P_{2}$ and $Q = P'_{1} \parallel P_{2}$, with $P_{1} \pired P'_{1}$.
By Definition \ref{def:tree} we have $\Tree(P)$ is over $\nset{P_1} \cup \nset{P_2} \cup \{\varepsilon\}$. By inductive hypothesis, we have that $\Tree(P'_{1})$ is over $\nset{P_1} \cup \{\varepsilon\}$. Hence we can conclude that $\Tree(Q)$ is over $\nset{P_1} \cup \nset{P_2} \cup \{\varepsilon\}$, thus $\Tree(Q) \in {\cal T}_{\{P\}}$.

 \item [Case \rulename{Act2}:] Analogous to the case for \rulename{Act1} and omitted. 

\item[Case \rulename{Loc}] 
Then $P = \component{a}{P_1}$ and $Q = \component{a}{P_1'}$, with $P_1 \pired P_1'$.
By Definition \ref{def:tree} we have $\Tree(P)$ is over $\nset{P_1} \cup \{a[\ ]\} \cup \{\varepsilon\}$. By inductive hypothesis, we have that $\Tree(P'_{1})$ is over $\nset{P_1} \cup \{\varepsilon\}$. Hence we can conclude that $\Tree(Q)$ is over $\nset{P_1} \cup \{a[\ ]\} \cup \{\varepsilon\}$, thus $\Tree(Q) \in {\cal T}_{\{P\}}$.

\item [Cases \rulename{Tau1}-\rulename{Tau2}:]
Then $P \equiv  \fillcont{C_1}{A}\parallel \fillcont{C_2}{B}$, where $C_{1}$ and $C_{2}$ are monadic contexts as in Definition \ref{d:mc}.
Moreover, 
$A$ is either 
$!b.Q$ or 
$\sum_{i \in I} \pi_i.Q_i$ with $\pi_{l}=b$, for some $l\in I$, and 
$B$ is either 
$!\outC{b}.R$
or $\sum_{i \in I} \pi_i.R_i$ with $\pi_{l}=\outC{b}$, for some $l\in I$.

We consider only the case in which $A = \sum_{i \in I} \pi_i.Q_i$ with $\pi_{l}=b$ and $B = !\outC{b}.R$;  the other cases are similar. 
Then $Q \equiv \fillcont{C_1}{Q_l}\parallel \fillcont{C_2}{R \parallel!\outC{b}.R }$. We know that  $\Tree(P)$ is over $\nset{C_1} \cup \nset{A} \cup \nset{C_2} \cup \nset{B} \cup \{\varepsilon\}$ and by noticing that $\nset{Q_l} \subseteq \nset{A}$ and $\nset{R \parallel!\outC{b}.R} \subseteq \nset{B}$ we can conclude that $\Tree(Q) \in {\cal T}_{\{P\}}$.

\item [Cases \rulename{Tau3}-\rulename{Tau4}:]
Then $P \equiv \fillcont{C_1}{A} \parallel \fillcont{C_2}{B}$ where:
\begin{itemize}
\item $C_{1}$ and $C_{2}$ are monadic contexts, as in Definition \ref{d:mc}; 
\item $A = \component{b}{P_1}$, for some $P_{1}$;  
\item $B  =  \sum_{i \in I} \pi_i.R_i$ with $\pi_{l}=\update{b}{\component{b}{U} \parallel P_2}$ for $l\in I$, or $ B = !\update{b}{U}.R$, for some $R$.
\end{itemize}

We consider the case in which $B = !\update{b}{\component{b}{U} \parallel P_2}.R$; the other case is similar. 
Then $Q \equiv \fillcont{C_1}{\fillcon{U}{P_1}}\parallel \fillcont{C_2}{R \parallel !\update{b}{U}.R }$.
 We know that  $\Tree(P)$ is over $\nset{C_1} \cup \nset{A} \cup \nset{C_2} \cup \nset{B} \cup \{\varepsilon\}$ and by noticing that $\nset{R \parallel !\update{b}{U}.R } \subseteq \nset{B}$ and that because of the restrictions on \evold{2} $P_3$ cannot occur behind a prefix, then  we can conclude that $\Tree(Q) \in {\cal T}_{\{P\}}$.
\end{description}
\end{proof}




Lemma \ref{lem:deriv} 
can be used to show that 
$\{\Tree(P) \mid P \in \deriv{S}\} \subseteq {\cal T}_{S}$, 
for some  set of processes $S$.
Then, using Theorem \ref{th:wqoccs} we can conclude that $\preceq$ is a wqo over it:

\begin{corollary}
  Let $S$ be a set of $\evold{2}$ processes. Then, $\preceq$ is a wqo over $\deriv{S}$.
\end{corollary}


The next result states 
%that %thing to show is that the well-quasi-ordering 
%$\preceq$ is strongly compatible 
strong compatibility of $\preceq$
with respect to reductions of \evold{2}. %defined above.


\begin{theorem}[Strong Compatibility]\label{th:scccs}
Let $P$ and $Q$ be \evold{2} processes such that $P \preceq Q$.
Then, $P \pired P'$ implies that there exists $Q'$ such that $Q \pired Q'$ and $P' \preceq Q'$. 
\end{theorem}
%\begin{proof}[Sketch]
\begin{proof}
By a case analysis on the reduction $P \pired P'$. 
It can be the result of either 
a \emph{input/output synchronization}---through rules \rulename{Tau1}/\rulename{Tau2}---
or 
an \emph{update synchronization}---through rules \rulename{Tau3}/\rulename{Tau4}).
In both cases, the reduction may be combined with uses of rule \rulename{Loc}, \rulename{Act1}, and \rulename{Act2}. % \todo{also rules act1, act
%\todo{check here}

We consider these two kinds of synchronizations  separately.
Let $n$ be a node with ancestor $m$, and let $\Tree(P)$ be a tree with root $\varepsilon$.
Below, when we say that $n$ \emph{is replaced by} $\Tree(P)$ we mean that: 
(i) $\varepsilon$ is merged with $m$; (ii) all children of $\varepsilon$ are added as siblings of $n$; and (iii) $n$ itself is removed.

%In the following when we say that a node $n$ is a replaced with a tree $\Tree(P)$  we mean that the root of $\Tree(P)$ (i.e. $\varepsilon$) is merged with the father of $n$,   all children of $\varepsilon$ are added as brothers of $n$ and $n$ itself is removed.


\begin{description}
\item[Input/output synchronization.] Then we have 
$$P \equiv D[A, B]$$ 
where
$D$ is a biadic context as in Definition \ref{d:mc}, $A$ is either 
$!a.P_1$ or 
$\sum_{i \in I} \pi_i.Q_i$ with $\pi_{l}=a$ and $Q_l = P_1$ for some $l\in I$, and 
$B$ is either 
$!\outC{a}.P_2$
or $\sum_{i \in I} \pi_i.R_i$ with $\pi_{l}=\outC{a}$ and $R_l = P_2$ , for some $l\in I$.

Consider the tree
$\Tree(P)$, and let $m$ and $n$ be two of its nodes, 
labeled $A$ and $B$, respectively.

We first consider the modifications to $\Tree(P)$ when $P \pired P'$. The tree $\Tree(P')$ is obtained from $\Tree(P)$ in the following way:
\begin{enumerate}
\item the node labeled $A$ is replaced with $\Tree(P_1)$; 
\item the node labeled $B$ is replaced with $\Tree(P_2)$.
\end{enumerate}

Since $P \preceq Q$, 
the definition of $\preceq$ 
ensures that there exists a mapping $f$ that associates nodes in $\Tree(P)$ to nodes in $\Tree(Q)$. 
In turn, this ensures the existence of a node $f(m)$ in $\Tree(Q)$ %that contains the 
labeled $A$. It also ensures the existence of a node $f(n)$ labeled $B$ and 
which has a common ancestor with $f(m)$. %\todo{perhaps $f(m)$ instead of $m$ here?}
Hence, the reduction can take place in $Q$ as well, and so $Q \pired Q'$.
Now, $\Tree(Q')$ is obtained from $\Tree(Q)$ by applying the same changes described above to the target nodes (of the input and the output) according to $f$.

The last thing to show is  $P' \preceq Q'$, which follows 
 by observing that the mapping between $\Tree(P')$ and $\Tree(Q')$ is necessarily the same mapping $f$  
 between $\Tree(P)$ and $\Tree(Q)$, for all the nodes that have not been modified by the reduction and 
 that there is a one-to-one correspondence for the other nodes, as the new trees $\Tree(P_1)$ and $\Tree(P_2)$ are added to both  $\Tree(P)$ and $\Tree(Q)$. 
Thus, $\Tree(P')=^{\mathsf{tr}} \Tree(Q')$. %\qed

\item[Update synchronization.] Then we have 
$$P \equiv D[\component{a}{P_1}, A]$$ 
where $D$ is a biadic context as in Definition \ref{d:mc} and  $A$ is either 
$!\update{a}{P_2}.R$ or 
$\sum_{i \in I} \pi_i.Q_i$ with $\pi_{l}=\update{a}{P_2}$ and $Q_l = R$ for some $l\in I$ .   
Consider the tree
$\Tree(P)$, and let $m$ and $n$ be two of its nodes, 
labeled $A$ and $\component{a}{\,}$ (with subtree $\Tree(P_1)$), respectively.

We first consider the modifications to $\Tree(P)$ when $P \pired P'$. The tree $\Tree(P')$ is obtained from $\Tree(P)$ in the following way:
\begin{enumerate}
\item the node labeled %in which 
$A$ %occurs 
is replaced with $\Tree(R)$; 
%\item the label $a$ corresponding to component $\component{a}{P_1}$ is replaced with $t$; 
%
\item as for the tree rooted in $a[\ ]$ 
%with subtree 
($\Tree(P_1)$), it is replaced with 
%subtree whose root is the child of the above node labeled %with label $t$ becomes 
$\Tree(\fillcon{P_2\,}{P_1})$. %, thus replacing $\Tree(\component{a}{P_1})$.
\end{enumerate}

Since $P \preceq Q$, 
the definition of $\preceq$ ensures that 
there exists a mapping $f$ that associates nodes in $\Tree(P)$ to nodes in $\Tree(Q)$. 
In turn, this ensures the existence of a node $f(m)$ in $\Tree(Q)$ %that contains the 
labeled $A$. It also ensures the existence of a node $f(n)$ labeled $a[\ ]$ and 
which has a common ancestor with $f(m)$. % \todo{perhaps $f(m)$ instead of $m$ here?}
Hence, the update synchronization above can take place in $Q$ as well, and so $Q \pired Q'$.
Now, $\Tree(Q')$ is obtained from $\Tree(Q)$ by applying the same changes described above to the target nodes (of the adaptable process $a$ and of the
update  in $A$) according to $f$.

The last thing to show is that $P' \preceq Q'$, which follows 
 by observing that the mapping between $\Tree(P')$ and $\Tree(Q')$ is the same mapping $f$  
 between $\Tree(P)$ and $\Tree(Q)$, for all the nodes that have not been modified by the reduction and 
 that there is a correspondence one to one for the other nodes. More precisely: 
\begin{enumerate}
 \item Consider the label in node $f(m)$: all nodes removed in $\Tree(P')$ have been removed in $\Tree(Q')$, hence nodes $m$ and $f(m)$ are still in relation.
%  \item Let us now consider the tree radicated in $f(n)$: Nodes do not disappear as the label $a$ is replaced with $t$ both in $n$ and $f(n)$.
%  Hence, it is not possible that two different levels are merged and the two nodes are still in relation.
 \item Finally, we consider the two trees rooted in $n$ and $f(n)$, namely 
 $S= \Tree(\fillcon{P_2\,}{P_1})$ and 
 $T=\Tree(\fillcon{P_2\,}{Q_1})$, respectively. $S$ is the same subtree as $T$ apart from some subtrees of $P_2$ and $Q_2$ that can be put easily in relation %as $t$ is the same in both subtrees and 
as the subtrees $\Tree(P_1)$ and $\Tree(Q_1)$ are in relation with $f$.
% Similarly as before the reserved name $t$ guarantees that different levels (not in relation with $f$) are merged.
 \end{enumerate}
Thus, $\Tree(P')=^{\mathsf{tr}} \Tree(Q')$. %\qed
\end{description}
\end{proof}


